Nuprl Lemma : map-wf2
11,40
postcript
pdf
A
,
B
:Type,
L
:(
A
List),
f
:({
x
:
A
| (
x
L
)}
B
). map(
f
;
L
)
(
B
List)
latex
Definitions
x
:
A
.
B
(
x
)
,
t
T
,
map(
f
;
as
)
,
Y
,
P
Q
,
guard(
T
)
,
prop{i:l}
,
P
Q
,
P
Q
,
P
Q
,
P
Q
Lemmas
l
member
wf
,
cons
member
origin
A,B:Type, L:(A List), f:({x:A| (x 
L)} 
B). map(f; L) (B List) A,B:Type, L:(A List), f:({x:A| (x L)} B). map(f; L) (B List) x:A. B(x) T
Q
Q
Q
Q Q